Inference at * 1 1 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
  (if 0 z x then x else -x fi  = if 0 z y then y else -y fi )  x =  y 

latex

 by InteriorProof ((((((BoolCasesOnCExp 0 z x) 
CollapseTHENM (BoolCasesOnCExp 0 z y))) 

CollapseTHENM (BoolCollapseTHENM (AbReduce 0))) 
CollapseTHENA ((Auto_aux (first_nat 1:n
CollapseTHENA ((Au) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 3. 0  x
C1: 4. 0  y
C1:   (x = y)  x =  y
C2: 

C2: 3. 0  x
C2: 4. y < 0
C2:   (x = (-y))  x =  y
C3: 

C3: 3. x < 0
C3: 4. 0  y
C3:   ((-x) = y)  x =  y
C4: 

C4: 3. x < 0
C4: 4. y < 0
C4:   ((-x) = (-y))  x =  y
C.

Definitions	T, P  Q, P & Q, P  Q, x:A. B(x), P  Q, True, ff, if b then t else f fi , , tt, t  T, Unit, ,
Lemmas	true wf, squash wf, assert of lt int, bnot of le int, eqff to assert, assert of le int, eqtt to assert, iff transitivity, bnot wf, lt int wf, le wf, assert wf, bool wf, le int wf